00010	VAR: x,y,z,u,v,X,Y,Z,U,V; INF_PRED: =,≤;INF_OP:/; PRE_OP: 0,1;
00015	EQUALITY: =;
00020	A1: x/y ≤ x ;
00050	
00100	DEF_OF_LESS: x ≤ y ≡ x/y = 0;
00300	A2: (x/z) /(y/z) ≤  (x/y)/z ;
00400	A3: 0 ≤ x ;
00500	
00600	A4: x ≤ y ∧ y ≤ x ⊃ x = y;
00700	A5: x ≤ 1; 
00750	T8: x ≤  y ⊃ x/z ≤ y/z;
00850	T11: 1/(1/x) = x/(1/x);
00900	T3: x/x  = 0; T1: x/1 =  0; T2: 0/x =  0;
01000	T5:   x ≤  y ∧  y ≤ z ⊃  x  ≤  z;
01100	T4: x/0 =  x;   
01150	T6: x/y ≤  z ⊃ x/z  ≤ y; 
01200	T7: x ≤  y ⊃ z/y  ≤ z/x;
01250	T9: 1/(1/(1/X))=1/X;
01300	T10: (1/X)/(1/(1/X))=1/X;
01400	THM: 1/x = 1/y ⊃ 1/(x/y) =  1;;
01500	
01600	
01700